usends1-p(es;ds;k;T;l;tg;B;f)
== (x:Id. vartype(source(l);x)  ds(x)?Top)
== & e@source(l). kind(e) = k  valtype(e)  T
== & (e:E. kind(e) = rcv(l,tg)  valtype(e)  B)
== & e@source(l).
== & kind(e) = k
== &  (e':E.
== &  (kind(e') = rcv(l,tg)
== &  (& sender(e') = e
== &  (& & (e'':E. kind(e'') = rcv(l,tg)  sender(e'') = e  e'' = e')
== &  (& & val(e') = f((state when e),val(e))) 

latex

---

clarification:

usends1-p(es;ds;k;T;l;tg;B;f)
== (x:Id. es-vartype(es; source(l); x)  fpf-cap(ds;IdDeq;x;Top))
== & alle-at(es;source(l);e.es-kind(es; e) = k  Knd  es-valtype(es; e)  T)
== & (e:es-E(es). es-kind(es; e) = rcv(l,tg)  Knd  es-valtype(es; e)  B)
== & alle-at(es;source(l);e.es-kind(es; e) = k  Knd
== & alle-at(es;source(l);e. (e':es-E(es).
== & alle-at(es;source(l);e. (es-kind(es; e') = rcv(l,tg)  Knd
== & alle-at(es;source(l);e. (& es-sender(es; e') = e  es-E(es)
== & alle-at(es;source(l);e. (& & (e'':es-E(es).
== & alle-at(es;source(l);e. (& & (es-kind(es; e'') = rcv(l,tg)  Knd
== & alle-at(es;source(l);e. (& & ( es-sender(es; e'') = e  es-E(es)
== & alle-at(es;source(l);e. (& & ( e'' = e'  es-E(es))
== & alle-at(es;source(l);e. (& & es-val(es; e')
== & alle-at(es;source(l);e. (& & =
== & alle-at(es;source(l);e. (& & f(es-state-when(es;e),es-val(es; e))
== & alle-at(es;source(l);e. (& &  B)) 

latex

Definitions	Id, vartype(i;x), f(x)?z, IdDeq, Top, valtype(e), e@i. P(e), source(l), x:A. B(x), A & B, P & Q, x:A. B(x), Knd, kind(e), rcv(l,tg), P  Q, sender(e), E, s = t, f(a), (state when e), val(e)
FDL editor aliases	usends1-p